Problem:
0(x1) -> 1(x1)
0(0(x1)) -> 0(x1)
3(4(5(x1))) -> 4(3(5(x1)))
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
0(1(1(1(1(1(0(1(1(0(0(1(1(0(1(1(1(0(1(0(1(1(0(1(0(1(1(1(1(0(1(1(0(1(
1
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
0
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
1
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
1
(
0
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
0(0(0(1(1(1(1(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1(1(0(1(0(0(0(0(1(1(1(0(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(1(0(1(0(1(0(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
1
(
1
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
1(0(1(0(1(1(1(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
41(21) -> 22*
31(20) -> 21*
51(19) -> 20*
51(23) -> 24*
11(9) -> 10*
11(11) -> 12*
00(2) -> 3*
00(1) -> 3*
10(2) -> 6*
10(1) -> 6*
30(2) -> 4*
30(1) -> 4*
40(2) -> 1*
40(1) -> 1*
50(2) -> 2*
50(1) -> 2*
20(2) -> 5*
20(1) -> 5*
1 -> 23,9
2 -> 19,11
10 -> 3*
12 -> 3*
22 -> 4*
24 -> 20*
problem:
Qed